i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da).
msg-spec-loc(snd;i)
 update-spec-decl(upd;ds)
 "ecl"  dom(ds)
 R-Feasible(ecl-machine at i with state ecl

 R-Feasible(A

 R-Feasible(state variables ds

 R-Feasible(actions da

 R-Feasible(sends snd

 R-Feasible(updates upd)
 (B:Realizer.
 (R-Feasible(B)
 ( (kecl-kinds(A) @ fpf-domain(da).
 ( (isrcv(k)
 ( ( (source(lnk(k)) = i  Id  Valtype(da;k)  R-da(B;destination(lnk(k)))(k)?Top)
 ( ( & (destination(lnk(k)) = i  Id  R-da(B;source(lnk(k)))(k)?Void  da(k)?Void))
 ( R-icompat(ecl-machine at i with state ecl

 ( R-icompat(A

 ( R-icompat(state variables ds

 ( R-icompat(actions da

 ( R-icompat(sends snd

 ( R-icompat(updates upd;B)) 

latex

Definitions

t  T, Top, x. t(x), x:A. B(x), a:A fp B(a), x.A(x), P  Q, x:AB(x), f(x), Void, lnk(k), source(l), f(x)?z, destination(l), Id, s = t, x:AB(x), P & Q, isrcv(k), b, x  dom(f), a = b, R-has-loc(R;i), , Prop, <a,b>, x:A. B(x), xdom(f). v=f(x)   P(x;v), ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), msg-spec-loc(snd;i), update-spec-decl(upd;ds), "$x", IdDeq, A, R-Feasible(R), Realizer, Valtype(da;k), R-icompat(A;B), xL. P(x), Knd, fpf-domain(f), ecl-kinds(x), as @ bs, (x  l), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, R-da(R;i), KindDeq, Type, f || g, P  Q, P  Q, x:A. B(x), Atom$n, rec(x.A(x)), es realizer ind, left+right, if b t else f fi, b, f(a), Unit

Lemmas

subtype rel transitivity, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, member append, ecl-machine-R-da-dom, l member wf, append wf, ecl-kinds wf, fpf-domain wf, ma-valtype wf, es realizer wf, R-Feasible wf, not wf, id-deq wf, update-spec-decl wf, msg-spec-loc wf, update-spec wf, msg-spec wf, ecl wf, R-icompat-one-loc, ecl-machine-loc, ecl-machine-R-da, bool wf, R-has-loc wf, eq id wf, fpf-dom wf, assert wf, isrcv wf, Id wf, ldst wf, fpf-cap wf, lsrc wf, lnk wf, fpf-ap wf, Kind-deq wf, fpf-trivial-subtype-top, R-da wf, ecl-machine wf, fpf wf, top wf, Knd wf